$\forall$$T$:Type\{i\}, $S$:(($\mathbb{N}\rightarrow$$T$)$\rightarrow\mathbb{P}$\{i'\}). $T$ $\Rightarrow$ generic\{i:l\}($T$; $f$.$S$($f$)) $\Rightarrow$ ($\exists$$f$:$\mathbb{N}\rightarrow$$T$. $S$($f$))